P:(). Dec(n:. ((P(n))))  (x: + Top. p-mu(P;x)) 

latex

ProofTree

Definitions	left + right, P  Q, Dec(P), s = t, t  T, , , x:AB(x), Type, f(a), x:A. B(x), b, , x:A  B(x), x:A. B(x), Top, p-mu(P;x), P  Q, A  B, a < b, , P & Q, i  j < k, {x:A| B(x)} , x.A(x), b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), x. t(x), False, A, i  j , -n, n+m, n - m, Void, |g|, S  T, #$n, {i..j}, inl x , inr x ,
Lemmas	ge wf, nat properties, nat ind tp, comp nat ind tp, decidable ex int seg, decidable assert, le wf, int seg wf, p-mu wf, top wf, decidable wf, assert wf, nat wf, bool wf